/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.ast;

import java.util.Iterator;

/**
 * Creates a pretty-printed String version of an Alloy formula.
 */
public class PrettyPrintVisitor extends ASTDepthFirstVisitor {
	
	/** current indentation level */
	private int _indent = 0;
	
	/** indent increment */
	private int _indInc = 2;
	
	/** current position in line */
	private int _curPos = 0;
	
	/** length of line.  <em>not</em> guaranteed to be respected. */
	private int _lineLength = 120;
	
	/** buffer for pretty-printed String */
	private StringBuffer _pPrintBuffer = new StringBuffer("\n");
	
	public String getPPrintString() {
		return _pPrintBuffer.toString();
	}
	
	/**
	 * Visit a node.  By default, just add the node's String.
	 */
	public void visit(Node node_) {
	    String nodeString = node_.nodeString();
	    
		_curPos += nodeString.length();
		_pPrintBuffer.append(nodeString); // should include strings of children
	}

	public void visit(FormulaSeq formSeq_) {
		_pPrintBuffer.append("{\n");
		_indent += _indInc;
		Iterator formulaIter = formSeq_.getFormulas().getFormulaIter();
		while (formulaIter.hasNext()) {
			Formula formula = (Formula)formulaIter.next();
			_addIndent();
			formula.applyVisitor(this);
			_pPrintBuffer.append("\n");
		}
		_indent -= _indInc;
		_addIndent();
		_pPrintBuffer.append("}");
	}
	
	public void visit(QuantifiedFormula quantForm_) {
		quantForm_.getQuantifier().applyVisitor(this);
		_pPrintBuffer.append(" ");
		quantForm_.getDecls().applyVisitor(this);
		_pPrintBuffer.append(" | ");
		quantForm_.getFormula().applyVisitor(this);
	}
	
	public void visit(ImplicationFormula implForm_) {
		implForm_.getIfFormula().applyVisitor(this);
		_pPrintBuffer.append(" => ");
		implForm_.getThenFormula().applyVisitor(this);
		if (!(implForm_.getElseFormula() instanceof EmptyFormula)) {
			_pPrintBuffer.append(" else ");
			implForm_.getElseFormula().applyVisitor(this);
		}
	}
	
	public void visit(NegFormula negForm_) {
		_pPrintBuffer.append("not ");
		negForm_.getFormula().applyVisitor(this);
	}
	
	public void visit(BinaryFormula binForm_) {
		binForm_.getLeft().applyVisitor(this);
		_pPrintBuffer.append(" ");
		binForm_.getOp().applyVisitor(this);
		_pPrintBuffer.append(" ");
		binForm_.getRight().applyVisitor(this);
	}
	private void _addIndent() {
		for (int i = 0; i < _indent; i++) {
			_pPrintBuffer.append(' ');
		}
	}
}
		

